\begin{tabbing}
$\forall$${\it es}$:ES, ${\it Sys}$:AbsInterface(Top), $L$:(E(${\it Sys}$) List), $j$:Id.
\\[0ex]loc{-}on{-}path(${\it es}$;$j$;$L$)
\\[0ex]$\Rightarrow$ ($\exists$\=$u$:E(${\it Sys}$)\+
\\[0ex]($\exists$$A$,$B$:E(${\it Sys}$) List. (loc($u$) = $j$ \& $L$ = ($A$ @ [$u$ / $B$]) \& ($\neg$loc{-}on{-}path(${\it es}$;$j$;$A$)))))
\-
\end{tabbing}